When a circuit is being designed, to verify the design of the circuit (or a component thereof), the circuit (or the component thereof) may undergo a process called formal verification. The purpose of formal verifications is to verify that the portion of the circuit being tested (referred to herein as the “component under test” or “CUT”) behaves as intended.
To perform formal verification, a set of inputs is applied to the CUT to produce a set of outputs. In response to applying the set of inputs to the CUT, if the set of outputs produced by the CUT (“the produced outputs”) do not conflict with a set of conditions established for the CUT, then the CUT passes formal verification. The set of conditions that the outputs of the CUT must meet are referred to as the “specification,” or the “properties,” of the CUT. Thus, when performing formal verification, the produced outputs of the CUT are verified to ensure that the produced outputs of the CUT conform to the specification, or the properties, of the CUT.
The inputs applied to the CUT during formal verification correspond to the inputs provided to the CUT in a real-world deployment. The circuitry providing the CUT with inputs is referred to as the “environment circuit”. To illustrate, consider FIG. 1, which is a block-diagram illustrating a circuit having an environment circuit and a CUT. As shown in FIG. 1, the outputs 102 produced by the environment circuit 112 correspond to the inputs 102 to the CUT 114.
When a CUT undergoes formal verification, the set of inputs applied to the CUT may be “constrained” by limiting the set of inputs applied to the CUT to those inputs the CUT would actually experience when the circuit is deployed. In this way, instead of applying all the possible inputs to the CUT when performing formal verification, only those inputs that the environment circuit would provide to the CUT in a real-world deployment are used. This process of restricting the set of inputs used in performing formal verification is called “constraining.” The motivation for constraining the inputs applied to the CUT is that the CUT may fail formal verification based on a set of inputs that the CUT will never experience in a real-world deployment. Thus, when performing formal verification, it is only necessary to test those inputs that the CUT will actually experience in a real-world deployment.
Typically, a circuit designer performs the process of constraining manually. That is, the circuit designer manually specifies inputs that can be applied to the CUT. However, it is possible for the circuit designer to either underconstrain or overconstrain the set of inputs that are applied to the CUT during formal verification.
If inputs, which the CUT will never experience in a real-world deployment, are applied to the CUT during formal verification, then the inputs applied to the CUT are said to be underconstrained. In other words, the CUT is being tested with more inputs than the CUT will actually experience in a real-world deployment. Typically, undercontraining the inputs applied to the CUT when performing formal verification does not create serious problems, because (a) if the CUT passes formal verification with the applied inputs being underconstrained, then the CUT is simply more robust than the CUT needs to be, and (b) undercontraining is relatively easy to detect since it often causes the CUT to fail formal verification since the CUT was never designed to operate under the inputs being applied.
On the other hand, overconstraining the inputs applied to the CUT during formal verification does present serious problems for the circuit designer. If less than all of the inputs that the CUT will experience in a real-world deployment are applied to the CUT during formal verification, then the inputs applied to the CUT are said to be overconstrained. In other words, the CUT is being tested with fewer inputs than the CUT will actually experience in a real-world deployment.
Overconstraining presents the danger that the circuit designer may reasonably conclude that the design of the CUT contains no errors since the CUT passed formal verification; however, since less than all of the inputs the CUT will experience in a real-world deployment were tested, it is possible that the CUT contains an error that will cause the CUT to not behave as intended when the untested inputs are applied to the CUT.
Currently, a circuit designer manually verifies that the inputs being applied to a CUT during formal verification are not underconstrained or overconstrained. Since this verification process is performed manually, it is susceptible to human error. Applicants are not aware of any existing mechanism or methodology that allows a set of constraints to be verified with certainty.
The approaches described in this section are approaches that could be pursued, but not necessarily approaches that have been previously conceived or pursued. Therefore, unless otherwise indicated, it should not be assumed that any of the approaches described in this section qualify as prior art merely by virtue of their inclusion in this section.